A certified type-preserving compiler from lambda calculus to assembly languageCHLIPALA, Adam.ACM SIGPLAN notices. 2007, Vol 42, Num 6, pp 54-65, issn 1523-2867, 12 p.Conference Paper

Modular development of certified program verifiers with a proof assistantCHLIPALA, Adam.ACM SIGPLAN notices. 2006, Vol 41, Num 9, pp 160-171, issn 1523-2867, 12 p.Conference Paper

A Verified Compiler for an Impure Functional LanguageCHLIPALA, Adam.ACM SIGPLAN notices. 2010, Vol 45, Num 1, pp 93-106, issn 1523-2867, 14 p.Conference Paper

Mostly-Automated Verification of Low-Level Programs in Computational Separation LogicCHLIPALA, Adam.ACM SIGPLAN notices. 2011, Vol 46, Num 6, pp 234-245, issn 1523-2867, 12 p.Conference Paper

Effective Interactive Proofs for Higher-Order Imperative ProgramsCHLIPALA, Adam; MALECHA, Gregory; MORRISETT, Greg et al.ACM SIGPLAN notices. 2009, Vol 44, Num 9, pp 79-90, issn 1523-2867, 12 p.Conference Paper

Parametric Higher-Order Abstract Syntax for Mechanized SemanticsCHLIPALA, Adam.ACM SIGPLAN notices. 2008, Vol 43, Num 9, pp 143-156, issn 1523-2867, 14 p.Conference Paper